the_es:event_system{i:l}, e,e':es-E(the_es).
es-le(the_es; e; e')
 ((((es-first(the_es; e'))) c es-le(the_es; e; es-pred(the_es; e')))  (e = e')) 

latex

Definitions	es-le(es; e; e'), False, event_system{i:l}, A, b, es-first(es; e), P  Q, P  Q, A c B, P  Q, guard(T), prop{i:l}, es-E(es), es-pred(es; e), P  Q, P  Q, es-locl(es; e; e'), x:A. B(x), t  T
Lemmas	es-locl wf, es-pred wf, es-E wf, es-locl-iff, es-first wf, assert wf, not wf, event system wf